(declare-fun a () Real)
(declare-fun b () Int)
(assert (and (> a 1) (= 0 (/ 1 a b))))
(check-sat)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(assert (> (/ 0.0 (+ 0.5 (ite (distinct a d) b c))) 0))
(check-sat)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (> (/ (+ c 1) (+ 0.5 (ite (= c 2) a b))) 2))
(check-sat)
(declare-const a Real)
(declare-const b Real)
(assert (and (= a 2) (or (= (/ 1 a) 0) (> b 0))))
(check-sat)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-const c Bool)
(assert (= (/ 0 (- 0.5 (ite c a b))) 1))
(check-sat)
